Inference at * 
Iof proof for Lemma adjacent-cons:


  T:Type, x, y, u:T, L:(T List).
  adjacent(T;[u / L];x;y)  ((0 < ||L||) & ((x = u & y = hd(L))  adjacent(T;L;x;y))) 

latex

 by ((RepUR``adjacent`` 0) 
CollapseTHEN (((MaAuto) 
CollapseTHEN (((ExRepD) 
CollapseTHEN (
CAuto')))))) 

latex

C1: 

C1: 1. T : Type
C1: 2. x : T
C1: 3. y : T
C1: 4. u : T
C1: 5. L : T List
C1: 6. i : {0..((||L||+1) - 1)}
C1: 7. x = [u / L][i]
C1: 8. y = [u / L][(i+1)]
C1: 9. 0 < ||L||
C1:   (x = u & y = hd(L))  (i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)]))
C2: 

C2: 1. T : Type
C2: 2. x : T
C2: 3. y : T
C2: 4. u : T
C2: 5. L : T List
C2: 6. 0 < ||L||
C2: 7. (x = u & y = hd(L))  (i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)]))
C2:   i:{0..((||L||+1) - 1)}. (x = [u / L][i] & y = [u / L][(i+1)])
C.

Definitions

adjacent(T;L;x;y), (x  l), x. t(x), x:A.B(x), (xL.P(x)), xL. P(x), |r|, x f y, f(a), a < b, |g|, a <p b, a  b, |p|, a ~ b, b | a, x,y:A//B(x;y), b, Atom, P  Q, Dec(P), i  j < k, A  B, A, False, <a, b>, x:A. B(x), P  Q, P  Q, x:AB(x), [car / cdr], hd(l), n - m, , l[i], n+m, A c B, , #$n, t  T, {x:A| B(x)} , , P  Q, left + right, a < b, type List, Type, x:A. B(x), P & Q, x:A  B(x), s = t, {i..j}, ||as||, i  j

Lemmas

iff wf, decidable ex int seg, decidable cand, select wf, rev implies wf, int seg wf